\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $L$:(Id List), ${\it del}$:rationals.
\\[0ex]fischer\=\{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2\}\+
\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\Rightarrow$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex]f{-}event\=\{x:ut2\}\+
\\[0ex](${\it es}$; $L$; $e$)
\-\\[0ex]$\Rightarrow$ (\=fischer{-}inv\=\{\=i:l,\+\+\+
\\[0ex]x:ut2,
\\[0ex]try:ut2,
\\[0ex]taken:ut2,
\\[0ex]contending:ut2,
\\[0ex]free:ut2,
\\[0ex]mine:ut2,
\\[0ex]wanted:ut2,
\\[0ex]z:ut2\}
\-\\[0ex](${\it es}$; $L$; ${\it del}$; $e$)
\-\\[0ex]$\in$ prop\{i:l\}))
\-\-
\end{tabbing}